$M$.rframe($k$ reads $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(IdDeq; (($M$.2.2.2.2.2.2.2.2.2.2).1); $x$; $x$,$L$.($\uparrow$deq{-}member(KindDeq;$k$;$L$)))